← 返回首页

#Lean 形式化

共 2 篇文章

杂谈

陶哲轩公开声援抵制 OpenAI：数学界与 AI 巨头矛盾升级 — AHM 声明"700 多份文件展示的是权力，不是学术研究"

2026-10-07 菲尔兹奖得主陶哲轩在博客转载"人类数学协会"（AHM）声明：呼吁数学家停止与 OpenAI 合作，批评其一次性发布 722 篇 AI 生成数学手稿"展示的是权力不是学术研究"。9 月底 OpenAI 在 GitHub 公开 372 个成果组覆盖千禧难题（准黎曼猜想 / 4 维挂谷 / 唯一博弈猜想），约 42% 已 Lean 形式化但已撤回 3 篇修订 14 篇。Scott Aaronson 妻子 Dana Moshkovitz（唯一博弈猜想专家）研读 OpenAI 论文后称"必须 AI 辅助才能读懂"。

陶哲轩Terence TaoAHM
杂谈

突发！Claude 拿下概率论「圣杯」，AI 跨过菲尔兹奖终点线 — 渗流连续相变猜想证明

2026-08-30，菲尔兹奖得主 Hugo Duminil-Copin 在博客里感慨"最著名的概率论猜想倒在 AI 推土机轰鸣下只是时间问题"，几乎同时 Anthropic 工程师 Justin Leder 在 GitHub 上传了 Claude 自动生成 + Lean 形式化严格验证的代码，70 年概率论圣杯——渗流连续相变猜想——被 AI 证明。猜想核心是 p=p_c 临界点上无限大连通网络能否形成（=0 连续 vs >0 突变），1980 年 Harry Kesten 2D 证明到 p_c=1/2，11 维及以上高维同样连续，3-10 维中间维度 70 年未解。

ClaudeAnthropic渗流理论